skip to main content
10.1145/1629335.1629343acmconferencesArticle/Chapter ViewAbstractPublication PagesesweekConference Proceedingsconference-collections
research-article

Refining the control structure of loops using static analysis

Published:12 October 2009Publication History

ABSTRACT

We present a simple yet useful technique for refining the control structure of loops that occur in imperative programs. Loops containing complex control flow are common in synchronous embedded controllers derived from modeling languages such as Lustre, Esterel, and Simulink/Stateflow. Our approach uses a set of labels to distinguish different control paths inside a given loop. The iterations of the loop are abstracted as a finite state automaton over these labels. Subsequently, we use static analysis techniques to identify infeasible iteration sequences and subtract such forbidden sequences from the initial language to obtain a refinement. In practice, the refinement of control flow sequences often simplifies the control flow patterns in the loop. We have applied the refinement technique to improve the precision of abstract interpretation in the presence of widening. Our experiments on a set of complex reactive loop benchmarks clearly show the utility of our refinement techniques. Abstraction interpretation with our refinement technique was able to verify all the properties for 10 out of the 13 benchmarks, while abstraction interpretation without refinement was able to verify only four. Other potentially useful applications include termination analysis and reverse engineering models from source code.

References

  1. Absint WCET timing analysis tool. http://www.absint.com/.Google ScholarGoogle Scholar
  2. Bagnara, R., Hill, P. M., Ricci, E., and Zaffanella, E. Precise widening operators for convex polyhedra. In Static Analysis Symposium (2003), vol. 2694 of LNCS, Springer, pp. 337--354. Google ScholarGoogle ScholarDigital LibraryDigital Library
  3. Balakrishnan, G., Sankaranarayanan, S., Ivancic, F., Wei, O., and Gupta, A. SLR: Path-sensitive analysis through infeasible-path detection and syntactic language refinement. In SAS (2008), vol. 5079 of LNCS, pp. 238--254. Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. Ball, T., and Rajamani, S. K. The SLAM toolkit. In CAV (2001), vol. 2102 of LNCS, pp. 260--264. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. Bardin, S., Finkel, A., Leroux, J., and Petrucci, L. FAST: Fast accelereation of symbolic transition systems. In CAV (July 2003), vol. 2725 of LNCS.Google ScholarGoogle Scholar
  6. Beyer, D., Henzinger, T. A., Jhala, R., and Majumdar, R. The software model checker BLAST. STTT 9, 5-6 (2007), 505--525. Google ScholarGoogle ScholarDigital LibraryDigital Library
  7. Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Mine, A., Monniaux, D., and Rival, X. A static analyzer for large safety-critical software. In PLDI (June 2003), pp. 196--207. Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. Clarke, E., Kroening, D., and Lerda, F. A tool for checking ANSI-C programs. In TACAS (2004), vol. 2988 of LNCS.Google ScholarGoogle Scholar
  9. Colon, M., Sankaranarayanan, S., and Sipma, H. Linear invariant generation using non-linear constraint solving. In CAV (July 2003), vol. 2725 of LNCS, Springer, pp. 420--433.Google ScholarGoogle Scholar
  10. Colon, M., and Sipma, H. Synthesis of linear ranking functions. In Tools and Algorithms for Construction and Analysis of Systems (April 2001), vol. 2031 of LNCS. Google ScholarGoogle ScholarDigital LibraryDigital Library
  11. Cook, B., Podelski, A., and Rybalchenko, A. Termination proofs for systems code. In PLDI (2006). Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. Cousot, P., and Cousot, R. Static determination of dynamic properties of programs. In Proc. ISOP'76 (1976), Dunod, Paris, France, pp. 106--130.Google ScholarGoogle Scholar
  13. Cousot, P., and Cousot, R. Abstract Interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL (1977), pp. 238--252. Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. Cousot, P., and Halbwachs, N. Automatic discovery of linear restraints among the variables of a program. In POPL'78 (Jan. 1978), pp. 84--97. Google ScholarGoogle ScholarDigital LibraryDigital Library
  15. Esparza, J., Hansel, D., Rossmanith, P., and Schwoon, S. Efficient algorithms for model checking pushdown systems. In CAV (2000), vol. 1855 of LNCS. Google ScholarGoogle ScholarDigital LibraryDigital Library
  16. Fehnker, A., Brauer, J., Huuck, R., and Seefried, S. Goanna: Syntactic software model checking. In Auto. Tech. for Verif.&Analysis (2008). Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. Gaubert, S., Goubault, E., Taly, A., and Zennou, S. Static analysis by policy iteration on relational domains. In ESOP (2007), vol. 4421 of LNCS, pp. 237--252. Google ScholarGoogle ScholarDigital LibraryDigital Library
  18. Gawlitza, T., and Seidl, H. Precise fixpoint computation through strategy iteration. In ESOP (2007), vol. 4421 of LNCS, pp. 300--315. Google ScholarGoogle ScholarDigital LibraryDigital Library
  19. Gopan, D., and Reps, T. W. Lookahead widening. In CAV (2006), vol. 4144 of LNCS, pp. 452--466. Google ScholarGoogle ScholarDigital LibraryDigital Library
  20. Gopan, D., and Reps, T. W. Guided static analysis. In SAS (2007), vol. 4634 of LNCS, pp. 349--365. Google ScholarGoogle ScholarDigital LibraryDigital Library
  21. Goubault, E., and Putot, S. Static analysis of numerical algorithms. In SAS (2006), vol. 4134 of LNCS, Springer, pp. 18--34. Google ScholarGoogle ScholarDigital LibraryDigital Library
  22. Gulwani, S., Jain, S., and Koskinen, E. Control-flow refinement and progress invariants for bound analysis. PLDI 2009 (to appear). Google ScholarGoogle ScholarDigital LibraryDigital Library
  23. Gupta, A., Henzinger, T. A., Majumdar, R., Rybalchenko, A., and Xu, R.-G. Proving non-termination. In POPL (2008), ACM, pp. 147--158. Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. Halbwachs, N. Synchronous programming of reactive systems. Kluwer Academic Pub., 1993. Google ScholarGoogle ScholarDigital LibraryDigital Library
  25. Halbwachs, N., Proy, Y., and Roumanoff, P. Verification of real-time systems using linear relation analysis. Formal Methods in System Design 11, 2 (1997), 157--185. Google ScholarGoogle ScholarDigital LibraryDigital Library
  26. Harary, F. Graph Theory. Addison-Wesley, 1969.Google ScholarGoogle Scholar
  27. Ivancic, F., Yang, Z., Ganai, M. K., Gupta, A., Shlyakhter, I., and Ashar, P. F-soft: Software verification platform. In CAV (2005), vol. 3576 of LNCS. Google ScholarGoogle ScholarDigital LibraryDigital Library
  28. Jeannet, B., Halbwachs, N., and Raymond, P. Dynamic partitioning in analyses of numerical properties. In Static Analysis Symposium, SAS'99 (Sep 1999), vol. 1694 of LNCS, pp. 39--50. Google ScholarGoogle ScholarDigital LibraryDigital Library
  29. MathWorks Inc. Electronic vehicle climate control simulink/stateflow model. www.mathworks.com/products/simulink/demos.html.Google ScholarGoogle Scholar
  30. Mathworks Inc. Simulink/stateflow (tm) model-based control design environment. Cf. www.mathworks.com/simulink.Google ScholarGoogle Scholar
  31. Mauborgne, L., and Rival, X. Trace partitioning in abstract interpretation based static analyzers. In ESOP (2005), vol. 3444 of LNCS, pp. 5--20. Google ScholarGoogle ScholarDigital LibraryDigital Library
  32. Min´e, A. A new numerical abstract domain based on difference-bound matrices. In PADO II (May 2001), vol. 2053 of LNCS, Springer, pp. 155--172. Google ScholarGoogle ScholarDigital LibraryDigital Library
  33. Sankaranarayanan, S., Ivancic, F., and Gupta, A. Program analysis using symbolic ranges. In SAS (2007), vol. 4634 of LNCS, pp. 366--383. Google ScholarGoogle ScholarDigital LibraryDigital Library
  34. Sankaranarayanan, S., Ivancic, F., Shlyakhter, I., and Gupta, A. Static analysis in disjunctive numerical domains. In SAS (2006), vol. 4134 of LNCS. Google ScholarGoogle ScholarDigital LibraryDigital Library
  35. Simon, A., and King, A. Widening polyhedra with landmarks. In APLAS (2006), vol. 4279 of LNCS. Google ScholarGoogle ScholarDigital LibraryDigital Library

Index Terms

  1. Refining the control structure of loops using static analysis

                Recommendations

                Comments

                Login options

                Check if you have access through your login credentials or your institution to get full access on this article.

                Sign in
                • Published in

                  cover image ACM Conferences
                  EMSOFT '09: Proceedings of the seventh ACM international conference on Embedded software
                  October 2009
                  332 pages
                  ISBN:9781605586274
                  DOI:10.1145/1629335

                  Copyright © 2009 ACM

                  Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

                  Publisher

                  Association for Computing Machinery

                  New York, NY, United States

                  Publication History

                  • Published: 12 October 2009

                  Permissions

                  Request permissions about this article.

                  Request Permissions

                  Check for updates

                  Qualifiers

                  • research-article

                  Acceptance Rates

                  EMSOFT '09 Paper Acceptance Rate33of106submissions,31%Overall Acceptance Rate60of203submissions,30%

                  Upcoming Conference

                  ESWEEK '24
                  Twentieth Embedded Systems Week
                  September 29 - October 4, 2024
                  Raleigh , NC , USA

                PDF Format

                View or Download as a PDF file.

                PDF

                eReader

                View online with eReader.

                eReader